$\forall$$A$, $B$:es\_realizer\{i:l\}, $P$, $Q$:(ES\{i\}$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$).
\\[0ex]$A$ $\Vdash$\{i\} ${\it es}$.$P$(${\it es}$) $\Rightarrow$ $B$ $\Vdash$\{i\} ${\it es}$.$Q$(${\it es}$) $\Rightarrow$ R{-}compat\{i:l\}($A$; $B$) $\Rightarrow$ $A$ $\oplus$ $B$ $\Vdash$\{i\} ${\it es}$.$P$(${\it es}$) \& $Q$(${\it es}$)